Nuprl Lemma : abmonoid_comm
13,42
postcript
pdf
g
:IAbMonoid,
a
,
b
:|
g
|. (
a
*
b
) = (
b
*
a
)
|
g
|
latex
Up
groups
1
Definitions of Statement
IAbMonoid
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
IAbMonoid
,
Comm(
T
;
op
)
Lemmas
iabmonoid
wf
,
iabmonoid
properties
origin
g:IAbMonoid, a, b:|g|. (a * b) = (b * a) 
|g| g:IAbMonoid, a, b:|g|. (a * b) = (b * a) |g| Tx:A. B(x)